/*
 * To change this license header, choose License Headers in Project Properties.
 * To change this template file, choose Tools | Templates
 * and open the template in the editor.
 */
package tp2ia_partie2;

import java.io.BufferedOutputStream;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.PrintStream;
import java.util.LinkedHashSet;
import java.util.Set;
import tp2ia_partie2.objects.*;

/**
 *
 * @author hp
 */
public class TP2IA_partie2_1 {

    /**
     * @param args the command line arguments
     */
    public static void main(String[] args) throws FileNotFoundException {
    //    System.setOut(new PrintStream(new BufferedOutputStream(new FileOutputStream("traceResolution.txt"))));

        /*
         *     Création de l'énoncé
         *     A->B , A , Prouver B   (Modus ponens)       
         */
        // C1 : A->B 
        Litteral A = new Litteral("A");
        Set<Litteral> faits = new LinkedHashSet<Litteral>();
        faits.add(A);
        Litteral B = new Litteral("B");
        Clause c1 = new RegleClause(faits, B);

        // C2 : B
        Clause c2 = new DefiniesClause(B);

        // C3 : Prouver B
        Clause c3 = new ButClause(B);

        // creation de l'ensemble BK
        Set<Clause> KB = new LinkedHashSet<Clause>();
        KB.add(c1);
        KB.add(c2);

        //lancement de la resolution
        Resolution_1 resolutionEngine = new Resolution_1();
        boolean resolutionResult = resolutionEngine.plResolution(KB, c3);

        System.out.println("\n\n ____RESULTAT_____");
        System.out.println(resolutionResult ? "But prouvé" : "But non prouvé");

    }

}
